theory Design_CloseSession
imports "../DesignSpec"
begin

section "auxiliary function"

definition tee_ta_close_session_teeDomain2_preR :: 
   "Sys_Config ⇒ StateR ⇒ SESSION_ID_TYPE option ⇒ CLIENT_TYPE option
   ⇒ PARAMS_TYPE option ⇒ PARAMS_TYPE option ⇒ StateR × TEE_RETURN_CODE_TYPE " where
  "tee_ta_close_session_teeDomain2_preR sc s tar_ses_id clientType params_in params_out ≡
      let s'= (tee_ta_close_session_teeDomain2_pre sc (⇑s) tar_ses_id clientType params_in params_out) in (s⇓(fst s'),(snd s'))
"

(**)
definition TA_CloseSessionEntryPointR::"StateR ⇒ THREAD_ID_TYPE ⇒ StateR" where
          "TA_CloseSessionEntryPointR s tid≡ 
                                         let s'=s⇓(TA_CloseSessionEntryPoint (⇑s) tid) in
                                                s'⦇IPC_driver:=IPC_driver s⦈"

section "TEEC_CloseSession"

definition TEEC_CloseSession1R :: "Sys_Config ⇒ StateR ⇒FD_TYPE⇒ SESSION_ID_TYPE option 
                                 ⇒ PARAMS_TYPE ⇒ PARAMS_TYPE 
                                 ⇒ (StateR × TEEC_RET_ORIGIN × TEEC_RETURN_CODE_TYPE)" where
          "TEEC_CloseSession1R sc s fd ses_id in_params out_params≡
                       let s'= (TEEC_CloseSession1 sc (⇑s) fd ses_id in_params out_params) in (s⇓(fst s'),fst(snd s'),snd(snd s'))"



(*return s_rev_event?*)
definition TEEC_CloseSession2R :: "Sys_Config ⇒ StateR ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE" where
          "TEEC_CloseSession2R sc s ≡ 
           let
                exec = (exec_prime s);
                p = fst (hd exec);
                ses_id = param1 p;
                client_type = param4 p;
                cmd_id = param6 p;
                in_params = param7 p;
                out_params = param8 p;
                s_rev_event = s⦇exec_prime := tl exec⦈;
                s_rev_event2 = Driver_Read s_rev_event smc_ex_init_read zx_mgr;
                pre_param_ops = TEE_pre_param_operation in_params;
                isSesIdinMgrSesIdList = isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s_rev_event))) (the ses_id);
                s_ret = (tee_ta_close_session_teeDomain2_preR sc s_rev_event2 ses_id client_type in_params out_params) 
             in
              if current s ≠ TEE sc then 
                (s, TEE_ORIGIN_TEE, TEE_ERROR_BAD_PARAMETERS)
              else if (exec_prime s) = [] then
                (s, TEE_ORIGIN_TEE, TEE_ERROR_BAD_PARAMETERS)
              else if snd (hd (exec_prime s)) ≠ TEEC_CS2 then
                (s, TEE_ORIGIN_TEE, TEE_ERROR_BAD_PARAMETERS)
              else if pre_param_ops ≠ TEE_SUCCESS then
                (s_rev_event, TEE_ORIGIN_TEE, TEE_ERROR_BAD_PARAMETERS)
              else if isSesIdinMgrSesIdList = False then
                (s_rev_event, TEE_ORIGIN_TEE, TEE_ERROR_BAD_PARAMETERS)
              else
                (fst s_ret, TEE_ORIGIN_TEE, snd s_ret) "

definition TEEC_CloseSession3R :: 
  "Sys_Config ⇒ StateR ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE " where
   "TEEC_CloseSession3R sc s ≡
   let
        exec = (exec_prime s);
        p = fst (hd exec);
        ses_id = param1 p;
        servTid = (param2 p);
        clientType = param4 p;
        in_params = param7 p;
        out_params = param8 p;
        s_rev_event = s⦇exec_prime := tl exec⦈;
        isSesIdInTaStateSesList = isSessIdInTaStateSessList (⇑s) ses_id servTid;
        nextFuncStepParam = ⦇param1 = ses_id, param2 = servTid, param3 = None, param4 = clientType,
               param5 = None, param6 =None, param7 = in_params, param8 = out_params, 
               param9 = None, param10=None, param11=None, param12=None, param13=None⦈;
        s_taCloseSessionEntry = TA_CloseSessionEntryPointR s_rev_event (the servTid);
        s_removeSess_inTaState = s_taCloseSessionEntry⇓(removeAllSessIdInTaStateSessList (⇑s_taCloseSessionEntry) (the ses_id) (the in_params) (the out_params));
        taState = (TAs_state s) (the servTid);
        taSesListInTaState = (TA_sessions (the taState));
        ta_attr = TA_attribute (the taState);
        isSingleInstance = singleInstance ta_attr;
        isKeepAlive = keepAlive ta_attr
     in
      if current s ≠ (the servTid) then 
        (s, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS)
      else if (exec_prime s) = [] then
        (s, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS)
      else if snd (hd (exec_prime s)) ≠ TEEC_CS3 then
        (s, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS)
      else if isSesIdInTaStateSesList = False then
        let
          s_sesIdNotInTaStateSesList = s_rev_event⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEEC_CS4)#(exec_prime s_rev_event)⦈
        in
        (s_sesIdNotInTaStateSesList, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS)
      else if ¬(isSingleInstance = True ∧ isKeepAlive = True) ∧ taSesListInTaState = [] then
        let
            s_taDestroyEntryPoint = (s_removeSess_inTaState⇓(TA_DestroyEntryPoint (⇑s_removeSess_inTaState)));
            s_deleteTaStateBackTEE = s_taDestroyEntryPoint⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEEC_CS4)#(exec_prime s_taDestroyEntryPoint)⦈
        in
        (s_deleteTaStateBackTEE, TEE_ORIGIN_TRUSTED_APP, TEE_SUCCESS)
      else 
        let
            s_notDeleteTaStateBackTEE = s_removeSess_inTaState⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEEC_CS4)#(exec_prime s_removeSess_inTaState)⦈
        in
        (s_notDeleteTaStateBackTEE, TEE_ORIGIN_TRUSTED_APP, TEE_SUCCESS)"

definition TEEC_CloseSession4R :: 
  "Sys_Config ⇒ StateR ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE " where
  "TEEC_CloseSession4R sc s ≡
  let
      exec = (exec_prime s);
      p = fst (hd exec);
      ses_id = param1 p;
      servTid = (param2 p);
      in_params = param7 p;
      out_params = param8 p;
      s_rev_event = s⦇exec_prime := tl exec⦈;
      mgrSes = the(findMgrSessionFromList (⇑s) (the ses_id));
      clientType = client_id mgrSes;
      loginType = login clientType;
      mgrTaInsList = mgr_ta_instances (ta_mgr (TEE_state s));
      curMgrTaIns = findTaInsInMgrByTid mgrTaInsList (the servTid);
      curMgrTaIns_attr = attribute (the curMgrTaIns);
      isSingleInstance = singleInstance curMgrTaIns_attr;
      isKeepAlive = keepAlive curMgrTaIns_attr;
      curMgrTaIns_refCnt = reference_cnt (the curMgrTaIns) - 1;
      s_removeSess_inMgrTaSes = s_rev_event⇓(removeAllSessionInMgrSesList (⇑s_rev_event) (the ses_id));
      s_setNotBusy = s_removeSess_inMgrTaSes⇓(setTaInsBusyByThreadId (⇑s_removeSess_inMgrTaSes) (the servTid) False);
      s_subRef = s_setNotBusy⇓(fst(subtractMgrInsRef (⇑s_setNotBusy) (the servTid)));
      s_subRefR = fst(Driver_Write_smc s_subRef zx_mgr ZX_OKr smc_ex_init)
  in
    if current s ≠ (TEE sc) then 
      (s, TEE_ORIGIN_TEE, TEE_ERROR_BAD_PARAMETERS)
    else if (exec_prime s) = [] then
      (s, TEE_ORIGIN_TEE, TEE_ERROR_BAD_PARAMETERS)
    else if snd (hd (exec_prime s)) ≠ TEEC_CS4 then
      (s, TEE_ORIGIN_TEE, TEE_ERROR_BAD_PARAMETERS)
    else if curMgrTaIns_refCnt = 0 ∧ (¬(isKeepAlive = True ∧ isSingleInstance = True) | loginType = DTC_IDENTITY) then
      let
         curTa_curTaSessionList = cur_ta_session_list (the curMgrTaIns);
         s_removeTaInTaIns = s_subRef⇓(fst(removeTaInsInMgrInsList (⇑s_subRef) (the servTid)));
         s_closeCurTaInsSessList = s_removeTaInTaIns⇓((addCloseSessionEvent2 sc (⇑s_removeTaInTaIns) (the in_params) (the out_params) curTa_curTaSessionList));
         s_teeState_deleteCurTa = s_closeCurTaInsSessList⇓(deleteTaStateByThreadId (⇑s_closeCurTaInsSessList) (the servTid));
         s_removeTaMemInTee = s_teeState_deleteCurTa⇓(removeTaMemInTeeDomain (⇑s_teeState_deleteCurTa) (the servTid));
         s_removeTaMemInTeeR = fst(Driver_Write_smc s_removeTaMemInTee zx_mgr ZX_OKr smc_ex_init)
      in
       (s_removeTaMemInTeeR, TEE_ORIGIN_TEE, TEE_SUCCESS)
    else 
      (s_subRefR, TEE_ORIGIN_TEE, TEE_SUCCESS)
  "

section "TEEC_CloseTASession"

definition TEE_CloseTASession1R :: "Sys_Config ⇒ StateR  
                                 ⇒ (StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE)" where
          "TEE_CloseTASession1R sc s≡
                       let s'= (TEE_CloseTASession1 sc (⇑s)) in (s⇓(fst s'),fst(snd s'),snd(snd s'))"

definition TEE_CloseTASession2R :: "Sys_Config ⇒ StateR ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE" where
          "TEE_CloseTASession2R sc s ≡ 
           let s'= (TEE_CloseTASession2 sc (⇑s)) in (s⇓(fst s'),fst(snd s'),snd(snd s'))"    

definition TEE_CloseTASession3R :: 
  "Sys_Config ⇒ StateR ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE " where
   "TEE_CloseTASession3R sc s ≡
   let
        exec = (exec_prime s);
        p = fst (hd exec);
        ses_id = param1 p;
        servTid = (param2 p);
        clientType = param4 p;
        in_params = param7 p;
        out_params = param8 p;
        s_rev_event = s⦇exec_prime := tl exec⦈;
        isSesIdInTaStateSesList = isSessIdInTaStateSessList (⇑s) ses_id servTid;
        nextFuncStepParam = ⦇param1 = ses_id, param2 = servTid, param3 = None, param4 = clientType,
               param5 = None, param6 =None, param7 = in_params, param8 = out_params, 
               param9 = None, param10=None, param11=None, param12=None, param13=None⦈;
        s_taCloseSessionEntry = TA_CloseSessionEntryPointR s_rev_event (the servTid);
        s_removeSess_inTaState = s_taCloseSessionEntry⇓(removeAllSessIdInTaStateSessList (⇑s_taCloseSessionEntry) (the ses_id) (the in_params) (the out_params));
        taState = (TAs_state s) (the servTid);
        taSesListInTaState = (TA_sessions (the taState));
        ta_attr = TA_attribute (the taState);
        isSingleInstance = singleInstance ta_attr;
        isKeepAlive = keepAlive ta_attr
     in
      if current s ≠ (the servTid) then 
        (s, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS)
      else if (exec_prime s) = [] then
        (s, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS)
      else if snd (hd (exec_prime s)) ≠ TEE_CS3 then
        (s, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS)
      else if isSesIdInTaStateSesList = False then
        let
          s_sesIdNotInTaStateSesList = s_rev_event⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEE_CS4)#(exec_prime s_rev_event)⦈
        in
        (s_sesIdNotInTaStateSesList, TEE_ORIGIN_TRUSTED_APP, TEE_ERROR_BAD_PARAMETERS)
      else if ¬(isSingleInstance = True ∧ isKeepAlive = True) ∧ taSesListInTaState = [] then
        let
            s_taDestroyEntryPoint = (s_removeSess_inTaState⇓(TA_DestroyEntryPoint (⇑s_removeSess_inTaState)));
            s_deleteTaStateBackTEE = s_taDestroyEntryPoint⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEE_CS4)#(exec_prime s_taDestroyEntryPoint)⦈
        in
        (s_deleteTaStateBackTEE, TEE_ORIGIN_TRUSTED_APP, TEE_SUCCESS)
      else 
        let
            s_notDeleteTaStateBackTEE = s_removeSess_inTaState⦇current := TEE sc, exec_prime := (nextFuncStepParam, TEE_CS4)#(exec_prime s_removeSess_inTaState)⦈
        in
        (s_notDeleteTaStateBackTEE, TEE_ORIGIN_TRUSTED_APP, TEE_SUCCESS)"

definition TEE_CloseTASession4R :: "Sys_Config ⇒ StateR ⇒ StateR × TEE_RETURN_ORIGIN_TYPE × TEE_RETURN_CODE_TYPE" where
          "TEE_CloseTASession4R sc s ≡ 
           let s'= (TEE_CloseTASession4 sc (⇑s)) in (s⇓(fst s'),fst(snd s'),snd(snd s'))"    

end